%\Section[dominator-modifier]{Combining Dominators and Modifiers}
%\input{dominator-modifier}


From abstract:

$~$ OIGJ is the first type system to unify the two main variants of ownership:
    owner-as-\emph{dominator}, which restricts aliasing,
    and owner-as-\emph{modifier}, which restricts modifications.
Thus, the programmer has the flexibility to choose whether
    the representation of an object
    cannot leak (the object \emph{dominates} the representation)
    or whether it may be freely shared as readonly (but only the owning object can
    \emph{modify} it).


From intro:
Restricting aliasing is not always desirable.
Sharing of objects is common practice, e.g.,
    collections with iterators, and
    the flyweight and model-view-controller patterns~\cite{designpatterns}.
Instead, %for applications such as program verification,
    it suffices to enforce the weaker \emph{owner-as-modifier}
    discipline~\cite{MuellerPoetzsch-Heffter99a,DietlDM2007}:
    an object can be \emph{mutated} only by its owner,
    but \emph{readonly} references can be shared without restriction.
This allows the owner to control state changes of its owned objects, for instance,
    in order to maintain invariants.

% \emph{Owner-as-modifier} relaxes owner-as-dominator by adding immutability
% information to ownership.

Previous work on ownership supported only one of these two disciplines.
OIGJ permits an a-la-carte approach:
    different objects in a program can obey different ownership disciplines,
    owner-as-dominator or owner-as-modifier,
    depending on the need.
Each object obeys just one ownership discipline and has exactly one owner.
That owner is either the dominator or modifier of the object.



  \item[Dominators and modifiers]
    The paper naturally unifies
    the two main ownership disciplines: owner-as-dominator and owner-as-modifier.
    In OIGJ, the owner generic parameter may be either \This{} or \Modifier{},
        denoting that the \this{} object is the dominator or modifier, respectively.

%\Ref{Section}{dominator-modifier} explains how owner-as-dominator and owner-as-modifier
%    were unified.





When adding Modifier, we need to add the following rules:
1) Cannot use Mutable fields (this simplifies a bit the NoVariant rule)

Modifier and Mutable together create problems:

class Foo<O,I> {
  Foo<Modifier,I> b = new Bar<Modifier,I>();
  Foo<O,Mutable> other = Foo<O,Mutable>();
}
Foo<World,Mutable> foo = new Foo<World,Mutable>();
Foo<World,ReadOnly> b = foo.b; // we perform view-point adaptation
b.other.other = new Foo<World,Mutable>(); // breaks owner-as-modifier!

2) owner parameter is variant for Modifier when ReadOnly:
Foo<Modifier,ReadOnly> f1;
Foo<World,ReadOnly> f2 = f1;

3) ownership nesting:
The owner parameter of a type must be lower or equal in the dominator tree
        compared to all other owner parameters inside that type.

4) View-point adaptation:
or (ii)~\code{f} is \this-owned and~$\code{o}\neq {\this}$,
        then the type of~\code{o.f} is adapted by replacing all immutability parameters
        that are not \Immutable{} with \ReadOnly{},
        and if~$\Ofn{\code{f}}=\underline{\This}$
        then we also replace all ownership parameters with the wildcard~\code{?}

5) \item[Inheritance]
    Consider the definition of a class or interface~\code{A}
        that extends or implements~\code{B}.
    Then~\code{B} cannot contain any fixed immutability or ownership parameters,
        i.e., it cannot contain \This,\Mutable, etc,
        but it can contain variables such as \code{O}, \code{I}, etc.

6) \item[Same-class subtype definition]
        and if $\hT_i$ is an owner parameter then $\hS_i=\hT_i$ or ($\hS_i=\Modifier$ and $\hT_i=\World$).







Next we define the connection between the \emph{compile-time}
    notion of the type parameters of \Ref{Figure}{owners-and-immutability-params}
    and the \emph{run-time} notions of \todo{immutability and owners}.
With respect to immutability, this connection is easier to grasp because
    there is an obvious mapping from immutability parameters to immutability of objects:
    each reference has an immutability parameter (at compile-time)
    that hints on the immutability of the object (at run-time).
Immutability parameter \Mutable/\Immutable imply the object is mutable/immutable,
    \ReadOnly imply the object may be either mutable or immutable and thus cannot be mutated,
    whereas \Raw imply the object is still raw and thus can still be mutated but after it is cooked,
    it might become immutable.

With respect to ownership, this connection is harder to grasp because
    \emph{owner parameters} (at compile-time) need to be mapped to \emph{owners} (which are objects at run-time).
Owner parameter~\This imply the object is owned by \this as a dominator (similarly for \Modifier),
    whereas~\World imply the object is owned by the root of the ownership tree
    (so the entire world can access and modify it).
Two references in the same class with the same owner parameter (at compile-time)
    will point to objects
    with the same owner (at run-time).
























\begin{figure*}[t]
\centering
\includegraphics[scale=0.8]{school}
\caption{
    (a) Object graph for the school-course example,
    (b) its \emph{ownership tree} with dominator and modifier edges, and
    (c) its \emph{dominator tree}.
}
\label{Figure:school}
\end{figure*}

This section explains about two variants of ownership supported in OIGJ:
    owner-as-dominator and owner-as-modifier.
It also formalize the runtime properties guaranteed by OIGJ.

To explain owner-as-modifier, we first need to define terms related to immutability.
Objects in OIGJ are either mutable or immutable.
OIGJ static type system guarantees the runtime property that the fields of an immutable objects
    cannot be reassigned after the object is cooked.
An object is cooked either when its constructor finishes (for a \this-owned
object) or when its owner is cooked.
References in OIGJ are either mutable, immutable, or readonly.
A readonly reference may point to a mutable or an immutable object, and it cannot be used
    to mutate the object (although the object might still be mutated by other aliases).

Ownership is used to enforce proper encapsulation in terms of aliasing or modifications,
    i.e., it ensures that an object cannot be aliased or modified outside its owner.
\Ref{Figure}{school}a presents an imaginary example describing
    school students that can enroll to different courses.
A school object contains a list of students.
A course object may point to students
    that are enrolled in the course.
All objects in this example are mutable.
We wish to use ownership in this example
    to restrict both aliasing and modification of objects:
    (i)~only the school may point to (or modify) the list, and
    (ii)~only the school may modify the students.
Phrased differently, a course cannot point to the list
%    but it can point to the students (without modifying them).
    nor modify the students, but it can point to (readonly) students.
To summarize, the school owns both the list and the students, but
    it owns the list as a \emph{dominator} (owner-as-dominator),
    and the students as a \emph{modifier} (owner-as-modifier).
\Ref{Section}{oigj-language} shows how OIGJ expresses such restrictions succinctly with the type:
\code{List<Dominator,Mutable,Student<Modifier,Mutable>>}



\Ref{Figure}{school}b shows the \emph{ownership tree},
    while \Ref{Figure}{school}c shows the \emph{dominator tree}.
The ownership tree constrains object modifications
    (whether one object can \emph{modify} another),
    and the dominator tree constrains heap structure (whether one object can
    \emph{point to} another).
Modifications must be done by the owner, no matter
    which ownership discipline is used.

The root of both trees is the \code{Stack} (the runtime execution stack),
    whose role is explained in \Ref{Section}{oigj-language}.
The ownership tree has two kinds of ownership edges,
    \emph{modifier} and \emph{dominator},
    corresponding to whether an object follows the owner-as-modifier or
    owner-as-dominator discipline.
For example, \Ref{Figure}{school}b shows that
    the school owns the students as a modifier and the list as a dominator.
%Therefore, the list may not leak outside of the school, but the
%    students may leak, e.g.,
%    a course object may point to enrolled students.
%However, a course may not modify a student.  %only the school may modify the students.

The ownership tree is defined by the programmer, by assigning each
    object an owner (either as a dominator or modifier).
To obtain the
    dominator tree, replace each modifier
    edge in the ownership tree by
    a dominator edge ending in \code{Stack}.
If an object is dominated by \code{Stack} (e.g., the students in
    \Ref{Figure}{school}c), it may be freely shared.
%Every dominator edge is implicitly a modifier edge, but if they coincide we
%    omit the modifier edge.

If the ownership tree only has dominator edges, then the owner and
the dominator are the same,
    and the whole program obeys the classical owner-as-dominator model.
On the other hand, if it only has modifier edges,
    then the dominator is always \code{Stack},
    and the whole program obeys the classical owner-as-modifier model.

In order to formalize the role of the dominator and ownership trees,
    we need to define some notation.
Given an object~$o$, its (direct) owner is~$O(o)$ and its (direct) dominator is~$D(o)$.
For example, $O(\code{aList})=\code{aSchool}$, $D(\code{aList})=\code{aSchool}$,
    $O(\code{aStudent}_1)=\code{aSchool}$, and $D(\code{aStudent}_1)=\code{Stack}$.
The ownership and dominator tree orders (both reflexive and transitive)
    are denoted by~$\preceq_O$ and~$\preceq_D$, respectively.
When~$o_1 \preceq_O o_2$, then
    we say that~$o_1$ is \emph{inside}~$o_2$, and~$o_2$ is \emph{outside}~$o_1$.
When~$o_1 \preceq_D o_2$, we say that~$o_2$ \emph{dominates}~$o_1$.
%If neither object is inside another, then we say the objects are \emph{incomparable}.

%Given objects~$o_1$ and~$o_2$, we say that~$o_1$ is a \emph{transitive owner} of~$o_2$
%    if~$o_1 \preceq_O O(o_2)$ (similarly for \emph{transitive dominator}).
%OIGJ guarantees the following runtime property:
%\emph{An object can be mutated only by its transitive owners,
%    and it can be pointed to only by its transitive dominators.}
%For example, the direct owner of \code{anEntry}$_1$ is \code{aList},
%    and the transitive owners of \code{anEntry}$_1$ are \code{aList} and its descendants such as \code{anEntry}$_n$.
%Therefore, \code{anEntry}$_1$ can point to (and mutate) \code{aList} and \code{anEntry}$_n$.
%Formally, we break down this property into heap and stack properties.


Consider two objects~$o$ and~$o'$.
OIGJ guarantees that: \\
\strut~~\textbf{Heap-property:}~$o'$ can point to~$o$ iff~$o' \preceq_D D(o)$. \\
\strut~~\textbf{Stack-property:}~$o$ can be mutated iff~$O(o)$ is on the call-stack.

The \emph{call-stack} is a stack of method's receivers, i.e., the \this objects of the methods on the stack.
The top of the call-stack is the receiver of the currently running method.
Specifically, the stack-property permits a method to mutate~$o$ if its receiver is~$O(o)$.
More generally, the stack-property also permits to mutate~$o$ if~$o'$ is anywhere on the call-stack (not just at the top),
    because~$o'$ might wish to delegate the mutation to another method.
For example, the owner of a collection may pass it to a sort method that mutates the collection; % that temporarily alias and mutate the collection
    this is allowed because the owner is on the call stack (although it is not at the top).
We say that sort is an \emph{owner-polymorphic method} because
    it is polymorphic in the (unknown) ownership of the collection.













A subtle point to note
    is that the type of a field~\code{f} might \emph{contain}
    the owner parameter \Modifier{}, but~$\Ofn{\code{f}} \neq \Modifier$,
    e.g., \code{List<O,I,Date<\underline{Modifier},I>}.
Assignment into such a field may only be done via \this as well.









The challenge is what to do when a \this-owned object escapes
    from \this.
Previous work prohibited such escape in owner-as-dominator (which is too restrictive),
    and changed the object to readonly in owner-as-modifier.
Universes~\cite{DietlDM2007} supports only owner-as-modifier,
    and the process of changing an object to readonly is called \emph{view-point adaptation}
    (because the view-point on the object changed from \this to the outside world).

OIGJ follows Universes approach and always allow an object to escape as readonly.
However, in owner-as-dominator, OIGJ ensures that the object cannot be stored on the heap,
    which will violate the owner-as-dominator property.
This is done in the last part of the rule by changing all the owner parameters to wildcards.

For example, consider an imaginary class \code{Rect},
    that is used to illustrate the process of view-point adaptation:

\begin{algorithmic}
\STATE \code{class Rect<\underline{O extends World},\underline{I extends ReadOnly}> \lb}
\STATE \code{~~boolean isEqualTo(Rect<?,ReadOnly> r) \lb}
\STATE \code{~~~~return this.p.x==\underline{r.p}.x \&\& this.p.y==\underline{r.p}.y; \rb}
\STATE \code{~~Point<\underline{Dominator},I> p;}
\STATE \COMMENT{Adapted: \code{Point<\underline{?},ReadOnly>}}
\STATE \code{~~Point<\underline{Modifier},I> modifierP;}
\STATE \COMMENT{Adapted: \code{Point<\underline{Modifier},ReadOnly>}}
\STATE \code{~~Point<\underline{Dominator},\underline{Immutable}> immutP;}
\STATE \COMMENT{Adapted: \code{Point<?,\underline{Immutable}>}}
\STATE \code{~~Point<\underline{O},I> peerP;}
\STATE \COMMENT{No adaptation needed because it is not \this-owned}
\STATE \code{~~List<\underline{O},I,Point<\underline{Modifier},I>> list;}
\STATE \COMMENT{Adapted: \code{List<\underline{O},ReadOnly,Point<\underline{Modifier},ReadOnly>>}}
\STATE \code{\rb}
\end{algorithmic}

Previous work on owner-as-dominator often use the example of a rectangle that owns its two points.
%    and therefore the rectangle can maintain the invariant that one point is always to the left of the other.
Field \code{p} is an example of such a \this-owned point.
Consider method \code{isEqualTo}, and compare the two field accesses: \code{this.p} and \code{r.p}.
The second access leaks the privately owned point, and therefore
    was considered illegal by previous work,
    thus leading to inefficient solutions that copy the private point.
OIGJ takes a different approach:
    the access \code{r.p} is allowed, but the point is leaked as readonly with a wildcard owner parameter,
    i.e.,~\code{Point<\underline{?},ReadOnly>},
    thus preventing anyone from mutating or storing the point on the heap.

In the above example, we wrote after each field its type after performing view-point adaptation,
    assuming it was accessed from a \code{Rect<O,I>}.
Note that we adapt the owner parameter to a wildcard only for \This, not for \Modifier.
Also, there is no need to replace \Immutable{} with \ReadOnly for
    \code{immutP}.
Finally, we note that view-point adaptation is applied recursively to the entire type,
    e.g., for field \code{list} we change both occurrences of \code{I} to \ReadOnly.
(The first occurrence of \code{I} was replaced as well to prevent mutating \code{list}
    and inserting a date with incorrect type.)

%For example, consider a \code{LinkedList} implementation with a
%   \this-owned field: \code{Entry<Dominator,I> header}.
%We have three possible cases of field assignment to consider:
%\begin{enumerate}
%  \item Accessing \code{header} via \this ,
%    i.e., the type of \code{\this.header} is \code{Entry<Dominator,I>}.
%  \item Access via an immutable (or readonly) list imposes
%    no restrictions
%    because the entry already cannot be mutated,
%    i.e., the type of \code{immutableList.header} is \code{Entry<Dominator,Immutable>}.
%  \item Access via another list returns a readonly entry, i.e.,
%    \code{Entry<Dominator,ReadOnly>}.
%\end{enumerate}

%We now define the \code{adapt} function,
%    that receives a type and either returns~$\bottom$ (meaning the access is illegal),
%    or it returns the view-point adaptation of the type.
%Formally,

%\Ref{Section}{formal} formally defines view-point adaptation.
%We note that the adaptation is first performed on the type of the field,
%    and only afterwards the generics are substituted.


\myparagraph{Inheritance}
OIGJ prohibits defining \emph{manifest classes},
    which are classes without an ownership or immutability parameter.
For instance, the following definition is illegal:\\
\code{class MutableDate<O extends World> extends}\\
\code{~~~~~~Date<O,Mutable> \lb~\rb}\\
Recall that view-point adaptation changes all immutability parameters to readonly
    in order to enforce owner-as-modifier.
%    \code{Date<Modifier,\underline{Mutable}>} changes to \code{Date<Modifier,\underline{ReadOnly}>}
Defining \code{MutableDate} is illegal because it lacks an immutability parameter.
More generally, the \textbf{Inheritance rule} prohibits any fixed immutability or ownership parameters in
    the supertype:
\begin{algorithmic}
\STATE \code{class MutableDateList<O,I,DateO> extends}
\STATE \code{~~~~~~List<O,I,Date<DateO,\underline{Mutable}>> \lb~\rb} \COMMENT{Illegal!}
\STATE \code{class DateList<O,I,DateO,DateI> extends}
\STATE \code{~~~~~~List<O,I,Date<DateO,DateI>> \lb~\rb} \COMMENT{Legal}
\end{algorithmic}

Manifest classes are usually used to save annotation overhead.
This overhead can be saved in OIGJ by using default annotations (\Ref{Section}{case-studies}).




Requiring that \emph{all} parameters are readonly can sometimes be too restrictive.
For example, consider the class \code{DateList<O,I,DateO,DateI>} defined above.
Then, \code{O} can change covariantly if \code{I} is readonly (irrelevant of \code{DateI}),
    however, \code{DateO} can only change covariantly if both \code{I} and \code{DateI} are readonly.
The subtyping rule could be relaxed further at the cost of maintaining relationship between
    immutability parameters and other parameters.
Bigger case studies are required in order to conclude if this is worthwhile.
Finally, note that covariance in the owner parameter is limited
    by the requirement that: $\hS_i=\hT_i$ or $\hS_i=\Modifier$.
E.g., \code{Date<\underline{Modifier},Mutable>} is a subtype of \code{Date<World,ReadOnly>},
    but \code{Date<\underline{Dominator},Mutable>} is not a subtype of \code{Date<World,\discretionary{}{}{}ReadOnly>}
    (because it could break owner-as-dominator).




Recall that OIGJ defines both an ownership tree and a dominator tree (see \Ref{Figure}{school}).
\emph{Ownership nesting} (for both owner-as-dominator and owner-as-modifier) is
    defined over the \emph{dominator tree} in order to prevent breaking the
    dominator property.
Recall that when the owner parameter is \Modifier or \World then the object is dominated by the \code{Stack}
    (the root of the dominator tree).
%Therefore, \This is strictly inside \Modifier.

% LocalWords:  readonly carte NoVariant ReadOnly params oigj aList aSchool iff
% LocalWords:  aStudent wildcards Rect boolean isEqualTo modifierP immutP peerP
% LocalWords:  MutableDate MutableDateList DateO DateList DateI
